\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, ${\it es}$:ES, $i$:Id, $e_{1}$, $e_{2}$:\{$e$:E$\mid$ loc($e$) $=$ $i$ \}, $L_{1}$,\+
\\[0ex]$L_{2}$:event{-}info(${\it ds}$;${\it da}$) List.
\-\\[0ex]$\neg$$L_{1}$ $=$ nil
\\[0ex]$\Rightarrow$ $\neg$$L_{2}$ $=$ nil
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. loc($e$) $=$ $i$ $\Rightarrow$ valtype($e$) $\subseteq\rho$ ${\it da}$(kind($e$))?Top)
\\[0ex]$\Rightarrow$ es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e_{2}$) $=$ ($L_{1}$ @ $L_{2}$) $\in$ event{-}info(${\it ds}$;${\it da}$) List
\\[0ex]$\Rightarrow$ $\exists$$e$$\in$($e_{1}$,$e_{2}$].es{-}hist\{i:l\}(${\it es}$;$e_{1}$;pred($e$)) $=$ $L_{1}$ \& es{-}hist\{i:l\}(${\it es}$;$e$;$e_{2}$) $=$ $L_{2}$
\end{tabbing}